Issue2247.agda:19,11-15
M1.x a != a of type A
when checking that the expression refl has type M1.x ≡ (λ a → a)
